standard bijections of Natural numbers#1249
Conversation
Co-authored-by: Naïm Camille Favier <n@monade.li>
| open import Cubical.Tactics.NatSolver | ||
| open import Cubical.Data.Nat.Bijections.IncreasingFunction | ||
|
|
||
| Triangle⊂ℕ = Σ[ k ∈ ℕ ] Σ[ i ∈ ℕ ] (i ≤ k) |
There was a problem hiding this comment.
This looks more like Triangle⊂ℕ×ℕ to me.
|
I changed |
| open import Cubical.Data.Sigma | ||
| open import Cubical.Data.Nat.Bijections.Triangle | ||
|
|
||
| Triangle⊂ℕ×ℕ≅ℕ×ℕ : Iso Triangle⊂ℕ×ℕ (ℕ × ℕ) |
There was a problem hiding this comment.
Looks like you could use totalEquiv from Cubical.Functions.Fibration here (as n ≤ m is definitionally the same as fiber (_+ n) m)
|
|
||
| private | ||
| 1+k+t=k+t+1 : (n : ℕ) → (t : ℕ ) → suc (n + t) ≡ n + suc t | ||
| 1+k+t=k+t+1 n t = solveℕ! |
There was a problem hiding this comment.
The solver here is also overkill, considering that this is exactly the type of +-suc
| open import Cubical.Data.Nat.Bijections.IncreasingFunction | ||
|
|
||
| double : ℕ → ℕ | ||
| double n = n + n |
There was a problem hiding this comment.
This is doubleℕ which is already defined in the library
|
|
||
| private | ||
| 2Sn=2n+2 : {n : ℕ} → double (suc n) ≡ double n + 2 | ||
| 2Sn=2n+2 = solveℕ! |
There was a problem hiding this comment.
This is also an instance of +-comm or +-suc, the solver is overkill
| sucIncreasing→StrictlyIncreasing {m = m} {n = n} (k , m+k+1=n) = | ||
| sucIncreasing→strictlyIncreasing' m n k m+k+1=n where | ||
|
|
||
| sucIncreasing→strictlyIncreasing' : |
There was a problem hiding this comment.
There is a lot of unnecessary whitespace between these lines
Also if you swap the positions of n and k here, you can use J>_ to simplify the proof a bit and avoid having to explicitly use subst
|
Well, I had some nitpciks, but seems im too late because its already merged |
4 participants
Added proofs showing that the type of natural numbers is isomorphic to it's own sum and product.